////////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009 The Mist project                                        //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
////////////////////////////////////////////////////////////////////////////////

///
/// \file
/// Contains the KeyInput wrapper.
/// Makes it possible to output an expression in the KeY language.
///

#ifndef KEYINPUT_HPP
#define KEYINPUT_HPP

////////////////////////////////////////////////////////////////////////////////
// Includes                                                                   //
////////////////////////////////////////////////////////////////////////////////

#include "common/outputproducer.hpp"
#include "common/ptr.hpp"
#include "common/types.hpp"

////////////////////////////////////////////////////////////////////////////////
// Forward Declarations                                                       //
////////////////////////////////////////////////////////////////////////////////

class Expression;

////////////////////////////////////////////////////////////////////////////////
// KeyInput Wrapper Class                                                     //
////////////////////////////////////////////////////////////////////////////////

/// Output decorator for a syntax tree node, which can produce a KeY expression
/// from the given Mist expression.
///
/// It is meant to be a temporary object,
/// used like this: <tt>cout << KeyInput(node);</tt>
///
class KeyInput : public OutputProducer {
	public:
		
		/// Build a KeyInput producing wrapper object.
		///
		KeyInput(
			wptr<Expression> tree ///< the subtree to produce a KeY expression from
		);
		
		ostream& send_to_stream(ostream& out) const;
	
	private:
		
		wptr<Expression> _expression;
};

#endif // KEYINPUT_HPP
